We continue Mizar formalization of general topology accordingto the book [11] by Engelking. In the article, we present the final theorem ofSection 4.1. Namely, the paper includes the formalization of theorems on thecorrespondence between the cardinalities of the basis and of some open subcover,and a discreet (closed) subspaces, and the weight of that metrizable topologicalspace. We also define Lindel¨of spaces and state the above theorem in this specialcase. We also introduce the concept of separation among two subsets (see [12]).
展开▼
